Matches in value-assignements (V): {{numOfValueMatches}}
Matches in edge-description: {{numOfDescriptionMatches}}
Rank |
Scope |
|||
-V- |
{{line.bestrank}}
|
{{line.desc}}
|
| Precondition (initial variable assignment): |
|
{{precondition}} |
| {{fault.rank}}. | {{fault.score}} | Details: | ||||
Current values:
|
||||||
1 | typedef enum { false, true } bool; |
2 | |
3 | extern int __VERIFIER_nondet_int(void); |
4 | |
5 | int main() { |
6 | int i; |
7 | int up; |
8 | i = __VERIFIER_nondet_int(); |
9 | up = 0; |
10 | |
11 | while (i > 0) { |
12 | if (i == 1) { |
13 | up = 1; |
14 | } |
15 | if (i == 10) { |
16 | up = 0; |
17 | } |
18 | if (up == 1) { |
19 | i = i+1; |
20 | } else { |
21 | i = i-1; |
22 | } |
23 | } |
24 | |
25 | return 0; |
26 | } |
| Date | Time | Level | Component | Message |
|---|---|---|---|---|
| 2025-08-27 | 13:26:10:820 | INFO | CPAMain.detectFrontendLanguageIfNecessary | Language C detected and set for analysis |
| 2025-08-27 | 13:26:10:905 | INFO | CPAchecker.run | CPAchecker 4.0 / terminationAnalysis (OpenJDK 64-Bit Server VM 17.0.15) started |
| 2025-08-27 | 13:26:10:924 | INFO | CPAchecker.parse | Parsing CFA from file(s) "Benchmarks/TermCOMP/C/Stroeder_15/Ex08/Ex08.c" |
| 2025-08-27 | 13:26:11:901 | INFO | CoreComponentsFactory.createAlgorithm | Using Restarting Algorithm |
| 2025-08-27 | 13:26:11:923 | WARNING | CPAchecker.printConfigurationWarnings | The following configuration options were specified but are not used: cpa.arg.lateMerge counterexample.export.exportWitness |
| 2025-08-27 | 13:26:11:924 | INFO | CPAchecker.runAlgorithm | Starting analysis ... |
| 2025-08-27 | 13:26:11:931 | INFO | RestartAlgorithm.run | Loading analysis 1 from file /cpachecker/config/components/combinations-parallel-termination.properties ... |
| 2025-08-27 | 13:26:11:976 | INFO | Analysis /cpachecker/config/components/combinations-parallel-termination.properties Parallel analysis 1 ResourceLimitChecker.fromConfiguration | Using the following resource limits: Thread CPU-time limit of 300s |
| 2025-08-27 | 13:26:12:355 | INFO | Analysis /cpachecker/config/components/combinations-parallel-termination.properties Parallel analysis 1 PredicateCPA PredicateCPA.<init> | Using predicate analysis with MathSAT5 version 5.6.10 (9293adc746be) (May 31 2023 12:38:06, gmp 6.2.0, gcc 7.5.0, 64-bit, reentrant) and JFactory 1.21. |
| 2025-08-27 | 13:26:12:670 | INFO | Analysis /cpachecker/config/components/combinations-parallel-termination.properties Parallel analysis 1 PredicateCPA PredicateCPARefiner.<init> | Using refinement for predicate analysis with PredicateAbstractionRefinementStrategy strategy. |
| 2025-08-27 | 13:26:12:680 | WARNING | CPAs.retrieveCPAOrFail | Warning: Skipping one analysis because the configuration file /cpachecker/config/components/combinations-parallel-termination.properties is invalid (TerminationAlgorithm needs a TerminationCPA) |
| 2025-08-27 | 13:26:12:682 | INFO | RestartAlgorithm.run | Loading analysis 1 from file /cpachecker/config/components/termination-recursion.properties ... |
| 2025-08-27 | 13:26:12:692 | INFO | NestingAlgorithm.checkConfigs | Mismatch of configuration options when loading from '/cpachecker/config/components/termination-recursion.properties': 'termination.config' has two values 'terminationAnalysis.properties' and 'termination-recursion.properties'. Using 'termination-recursion.properties'. |
| 2025-08-27 | 13:26:12:717 | WARNING | Analysis /cpachecker/config/components/termination-recursion.properties PredicateCPA FormulaManagerView.<init> | Using unsound approximation of ints with unbounded integers and floats with rationals for encoding program semantics. |
| 2025-08-27 | 13:26:12:721 | INFO | Analysis /cpachecker/config/components/termination-recursion.properties PredicateCPA PredicateCPA.<init> | Using predicate analysis with MathSAT5 version 5.6.10 (9293adc746be) (May 31 2023 12:38:06, gmp 6.2.0, gcc 7.5.0, 64-bit, reentrant) and JFactory 1.21. |
| 2025-08-27 | 13:26:12:831 | INFO | Analysis /cpachecker/config/components/termination-recursion.properties PredicateCPA PredicateCPARefiner.<init> | Using refinement for predicate analysis with PredicateAbstractionRefinementStrategy strategy. |
| 2025-08-27 | 13:26:12:896 | WARNING | Analysis /cpachecker/config/components/termination-recursion.properties FormulaManagerView.<init> | Using unsound approximation of ints with unbounded integers and floats with rationals for encoding program semantics. |
| 2025-08-27 | 13:26:12:932 | INFO | RestartAlgorithm.run | Starting analysis 1 ... |
| 2025-08-27 | 13:26:12:933 | INFO | Analysis /cpachecker/config/components/termination-recursion.properties TerminationAlgorithm.run0 | Starting termination algorithm. |
| 2025-08-27 | 13:26:17:236 | WARNING | Analysis /cpachecker/config/components/termination-recursion.properties TerminationAlgorithm.proveLoopTermination | Could not synthesize a termination or non-termination argument. |
| 2025-08-27 | 13:26:18:693 | WARNING | Analysis /cpachecker/config/components/termination-recursion.properties TerminationAlgorithm.proveLoopTermination | Could not synthesize a termination or non-termination argument. |
| 2025-08-27 | 13:26:20:373 | WARNING | Analysis /cpachecker/config/components/termination-recursion.properties TerminationAlgorithm.proveLoopTermination | Could not synthesize a termination or non-termination argument. |
| 2025-08-27 | 13:26:21:957 | WARNING | Analysis /cpachecker/config/components/termination-recursion.properties TerminationAlgorithm.proveLoopTermination | Could not synthesize a termination or non-termination argument. |
| 2025-08-27 | 13:26:23:698 | WARNING | Analysis /cpachecker/config/components/termination-recursion.properties TerminationAlgorithm.proveLoopTermination | Could not synthesize a termination or non-termination argument. |
| 2025-08-27 | 13:26:25:628 | WARNING | Analysis /cpachecker/config/components/termination-recursion.properties TerminationAlgorithm.proveLoopTermination | Could not synthesize a termination or non-termination argument. |
| 2025-08-27 | 13:26:27:110 | WARNING | Analysis /cpachecker/config/components/termination-recursion.properties TerminationAlgorithm.proveLoopTermination | Could not synthesize a termination or non-termination argument. |
| 2025-08-27 | 13:26:28:811 | WARNING | Analysis /cpachecker/config/components/termination-recursion.properties TerminationAlgorithm.proveLoopTermination | Could not synthesize a termination or non-termination argument. |
| 2025-08-27 | 13:26:30:002 | WARNING | Analysis /cpachecker/config/components/termination-recursion.properties TerminationAlgorithm.proveLoopTermination | Could not synthesize a termination or non-termination argument. |
| 2025-08-27 | 13:26:31:640 | WARNING | Analysis /cpachecker/config/components/termination-recursion.properties TerminationAlgorithm.proveLoopTermination | Could not synthesize a termination or non-termination argument. |
| 2025-08-27 | 13:26:33:472 | WARNING | Analysis /cpachecker/config/components/termination-recursion.properties TerminationAlgorithm.proveLoopTermination | Could not synthesize a termination or non-termination argument. |
| 2025-08-27 | 13:26:34:712 | WARNING | Analysis /cpachecker/config/components/termination-recursion.properties TerminationAlgorithm.proveLoopTermination | Could not synthesize a termination or non-termination argument. |
| 2025-08-27 | 13:26:36:430 | WARNING | Analysis /cpachecker/config/components/termination-recursion.properties TerminationAlgorithm.proveLoopTermination | Could not synthesize a termination or non-termination argument. |
| 2025-08-27 | 13:26:38:276 | WARNING | Analysis /cpachecker/config/components/termination-recursion.properties TerminationAlgorithm.proveLoopTermination | Could not synthesize a termination or non-termination argument. |
| 2025-08-27 | 13:26:40:086 | WARNING | Analysis /cpachecker/config/components/termination-recursion.properties TerminationAlgorithm.proveLoopTermination | Could not synthesize a termination or non-termination argument. |
| 2025-08-27 | 13:26:41:304 | WARNING | Analysis /cpachecker/config/components/termination-recursion.properties TerminationAlgorithm.proveLoopTermination | Could not synthesize a termination or non-termination argument. |
| 2025-08-27 | 13:26:43:832 | WARNING | Analysis /cpachecker/config/components/termination-recursion.properties TerminationAlgorithm.proveLoopTermination | Could not synthesize a termination or non-termination argument. |
| 2025-08-27 | 13:26:45:357 | WARNING | Analysis /cpachecker/config/components/termination-recursion.properties TerminationAlgorithm.proveLoopTermination | Could not synthesize a termination or non-termination argument. |
| 2025-08-27 | 13:26:46:675 | WARNING | Analysis /cpachecker/config/components/termination-recursion.properties TerminationAlgorithm.proveLoopTermination | Could not synthesize a termination or non-termination argument. |
| 2025-08-27 | 13:26:48:379 | WARNING | Analysis /cpachecker/config/components/termination-recursion.properties TerminationAlgorithm.proveLoopTermination | Could not synthesize a termination or non-termination argument. |
| 2025-08-27 | 13:26:49:678 | WARNING | Analysis /cpachecker/config/components/termination-recursion.properties TerminationAlgorithm.proveLoopTermination | Could not synthesize a termination or non-termination argument. |
| 2025-08-27 | 13:26:51:328 | WARNING | Analysis /cpachecker/config/components/termination-recursion.properties TerminationAlgorithm.proveLoopTermination | Could not synthesize a termination or non-termination argument. |
| 2025-08-27 | 13:26:53:021 | WARNING | Analysis /cpachecker/config/components/termination-recursion.properties TerminationAlgorithm.proveLoopTermination | Could not synthesize a termination or non-termination argument. |
| 2025-08-27 | 13:26:55:743 | WARNING | Analysis /cpachecker/config/components/termination-recursion.properties TerminationAlgorithm.proveLoopTermination | Could not synthesize a termination or non-termination argument. |
| 2025-08-27 | 13:26:57:129 | WARNING | Analysis /cpachecker/config/components/termination-recursion.properties TerminationAlgorithm.proveLoopTermination | Could not synthesize a termination or non-termination argument. |
| 2025-08-27 | 13:26:58:810 | WARNING | Analysis /cpachecker/config/components/termination-recursion.properties TerminationAlgorithm.proveLoopTermination | Could not synthesize a termination or non-termination argument. |
| 2025-08-27 | 13:27:02:246 | WARNING | Analysis /cpachecker/config/components/termination-recursion.properties TerminationAlgorithm.proveLoopTermination | Could not synthesize a termination or non-termination argument. |
| 2025-08-27 | 13:27:03:709 | WARNING | Analysis /cpachecker/config/components/termination-recursion.properties TerminationAlgorithm.proveLoopTermination | Could not synthesize a termination or non-termination argument. |
| 2025-08-27 | 13:27:06:558 | WARNING | Analysis /cpachecker/config/components/termination-recursion.properties TerminationAlgorithm.proveLoopTermination | Could not synthesize a termination or non-termination argument. |
| 2025-08-27 | 13:27:08:641 | WARNING | Analysis /cpachecker/config/components/termination-recursion.properties TerminationAlgorithm.proveLoopTermination | Could not synthesize a termination or non-termination argument. |
| 2025-08-27 | 13:27:10:046 | WARNING | Analysis /cpachecker/config/components/termination-recursion.properties TerminationAlgorithm.proveLoopTermination | Could not synthesize a termination or non-termination argument. |
| 2025-08-27 | 13:27:11:987 | WARNING | Analysis /cpachecker/config/components/termination-recursion.properties TerminationAlgorithm.proveLoopTermination | Could not synthesize a termination or non-termination argument. |
| 2025-08-27 | 13:27:13:935 | WARNING | Analysis /cpachecker/config/components/termination-recursion.properties TerminationAlgorithm.proveLoopTermination | Could not synthesize a termination or non-termination argument. |
| 2025-08-27 | 13:27:16:828 | WARNING | Analysis /cpachecker/config/components/termination-recursion.properties TerminationAlgorithm.proveLoopTermination | Could not synthesize a termination or non-termination argument. |
| 2025-08-27 | 13:27:18:186 | WARNING | Analysis /cpachecker/config/components/termination-recursion.properties TerminationAlgorithm.proveLoopTermination | Could not synthesize a termination or non-termination argument. |
| 2025-08-27 | 13:27:20:134 | WARNING | Analysis /cpachecker/config/components/termination-recursion.properties TerminationAlgorithm.proveLoopTermination | Could not synthesize a termination or non-termination argument. |
| 2025-08-27 | 13:27:23:510 | WARNING | Analysis /cpachecker/config/components/termination-recursion.properties TerminationAlgorithm.proveLoopTermination | Could not synthesize a termination or non-termination argument. |
| 2025-08-27 | 13:27:25:121 | WARNING | Analysis /cpachecker/config/components/termination-recursion.properties TerminationAlgorithm.proveLoopTermination | Could not synthesize a termination or non-termination argument. |
| 2025-08-27 | 13:27:27:603 | WARNING | Analysis /cpachecker/config/components/termination-recursion.properties TerminationAlgorithm.proveLoopTermination | Could not synthesize a termination or non-termination argument. |
| 2025-08-27 | 13:27:30:411 | WARNING | Analysis /cpachecker/config/components/termination-recursion.properties TerminationAlgorithm.proveLoopTermination | Could not synthesize a termination or non-termination argument. |
| 2025-08-27 | 13:27:32:361 | WARNING | Analysis /cpachecker/config/components/termination-recursion.properties TerminationAlgorithm.proveLoopTermination | Could not synthesize a termination or non-termination argument. |
| 2025-08-27 | 13:27:35:022 | WARNING | Analysis /cpachecker/config/components/termination-recursion.properties TerminationAlgorithm.proveLoopTermination | Could not synthesize a termination or non-termination argument. |
| 2025-08-27 | 13:27:37:234 | WARNING | Analysis /cpachecker/config/components/termination-recursion.properties TerminationAlgorithm.proveLoopTermination | Could not synthesize a termination or non-termination argument. |
| 2025-08-27 | 13:27:40:853 | WARNING | Analysis /cpachecker/config/components/termination-recursion.properties TerminationAlgorithm.proveLoopTermination | Could not synthesize a termination or non-termination argument. |
| 2025-08-27 | 13:27:42:174 | WARNING | Analysis /cpachecker/config/components/termination-recursion.properties TerminationAlgorithm.proveLoopTermination | Could not synthesize a termination or non-termination argument. |
| 2025-08-27 | 13:27:44:758 | WARNING | Analysis /cpachecker/config/components/termination-recursion.properties TerminationAlgorithm.proveLoopTermination | Could not synthesize a termination or non-termination argument. |
| 2025-08-27 | 13:27:48:437 | WARNING | Analysis /cpachecker/config/components/termination-recursion.properties TerminationAlgorithm.proveLoopTermination | Could not synthesize a termination or non-termination argument. |
| 2025-08-27 | 13:27:50:060 | WARNING | Analysis /cpachecker/config/components/termination-recursion.properties TerminationAlgorithm.proveLoopTermination | Could not synthesize a termination or non-termination argument. |
| 2025-08-27 | 13:27:53:075 | WARNING | Analysis /cpachecker/config/components/termination-recursion.properties TerminationAlgorithm.proveLoopTermination | Could not synthesize a termination or non-termination argument. |
| 2025-08-27 | 13:27:54:824 | WARNING | Analysis /cpachecker/config/components/termination-recursion.properties TerminationAlgorithm.proveLoopTermination | Could not synthesize a termination or non-termination argument. |
| 2025-08-27 | 13:27:57:949 | WARNING | Analysis /cpachecker/config/components/termination-recursion.properties TerminationAlgorithm.proveLoopTermination | Could not synthesize a termination or non-termination argument. |
| 2025-08-27 | 13:27:59:661 | WARNING | Analysis /cpachecker/config/components/termination-recursion.properties TerminationAlgorithm.proveLoopTermination | Could not synthesize a termination or non-termination argument. |
| 2025-08-27 | 13:28:01:745 | WARNING | Analysis /cpachecker/config/components/termination-recursion.properties TerminationAlgorithm.proveLoopTermination | Could not synthesize a termination or non-termination argument. |
| 2025-08-27 | 13:28:03:367 | WARNING | Analysis /cpachecker/config/components/termination-recursion.properties TerminationAlgorithm.proveLoopTermination | Could not synthesize a termination or non-termination argument. |
| 2025-08-27 | 13:28:06:977 | WARNING | Analysis /cpachecker/config/components/termination-recursion.properties TerminationAlgorithm.proveLoopTermination | Could not synthesize a termination or non-termination argument. |
| 2025-08-27 | 13:28:08:890 | WARNING | Analysis /cpachecker/config/components/termination-recursion.properties TerminationAlgorithm.proveLoopTermination | Could not synthesize a termination or non-termination argument. |
| 2025-08-27 | 13:28:10:533 | WARNING | Analysis /cpachecker/config/components/termination-recursion.properties TerminationAlgorithm.proveLoopTermination | Could not synthesize a termination or non-termination argument. |
| 2025-08-27 | 13:28:13:034 | WARNING | Analysis /cpachecker/config/components/termination-recursion.properties TerminationAlgorithm.proveLoopTermination | Could not synthesize a termination or non-termination argument. |
| 2025-08-27 | 13:28:14:637 | WARNING | Analysis /cpachecker/config/components/termination-recursion.properties TerminationAlgorithm.proveLoopTermination | Could not synthesize a termination or non-termination argument. |
| 2025-08-27 | 13:28:19:597 | WARNING | Analysis /cpachecker/config/components/termination-recursion.properties TerminationAlgorithm.proveLoopTermination | Could not synthesize a termination or non-termination argument. |
| 2025-08-27 | 13:28:21:672 | WARNING | Analysis /cpachecker/config/components/termination-recursion.properties TerminationAlgorithm.proveLoopTermination | Could not synthesize a termination or non-termination argument. |
| 2025-08-27 | 13:28:23:502 | WARNING | Analysis /cpachecker/config/components/termination-recursion.properties TerminationAlgorithm.proveLoopTermination | Could not synthesize a termination or non-termination argument. |
| 2025-08-27 | 13:28:25:588 | WARNING | Analysis /cpachecker/config/components/termination-recursion.properties TerminationAlgorithm.proveLoopTermination | Could not synthesize a termination or non-termination argument. |
| 2025-08-27 | 13:28:27:248 | WARNING | Analysis /cpachecker/config/components/termination-recursion.properties TerminationAlgorithm.proveLoopTermination | Could not synthesize a termination or non-termination argument. |
| 2025-08-27 | 13:28:28:953 | WARNING | Analysis /cpachecker/config/components/termination-recursion.properties TerminationAlgorithm.proveLoopTermination | Could not synthesize a termination or non-termination argument. |
| 2025-08-27 | 13:28:29:593 | INFO | Analysis /cpachecker/config/components/termination-recursion.properties CounterexampleCheckAlgorithm.checkCounterexample | Error path found, starting counterexample check with CPACHECKER. |
| 2025-08-27 | 13:28:30:047 | WARNING | Analysis /cpachecker/config/components/termination-recursion.properties CounterexampleCheck AutomatonGraphmlParser.getSpecAsProperties | Cannot map specification TRUE to property type. Will ignore it (would only be problematic if this were the termination property). |
| 2025-08-27 | 13:28:30:081 | WARNING | Analysis /cpachecker/config/components/termination-recursion.properties CounterexampleCheck AutomatonGraphmlParser.collectEdgeData | Source A17144 of transition [edge: null] is a violation state. No outgoing edges expected. |
| 2025-08-27 | 13:28:30:136 | INFO | Analysis /cpachecker/config/components/termination-recursion.properties CounterexampleCheck PredicateCPA PredicateCPA.<init> | Using predicate analysis with MathSAT5 version 5.6.10 (9293adc746be) (May 31 2023 12:38:06, gmp 6.2.0, gcc 7.5.0, 64-bit, reentrant). |
| 2025-08-27 | 13:41:09:404 | WARNING | ShutdownNotifier.shutdownIfNecessary | Warning: Analysis interrupted (The JVM is shutting down, probably because Ctrl+C was pressed.) |
| 2025-08-27 | 13:41:09:406 | WARNING | ForceTerminationOnShutdown$1.shutdownRequested | Shutdown requested (The JVM is shutting down, probably because Ctrl+C was pressed.), waiting for termination. |
| Statistics Name | Statistics Value | Additional Value |
|---|---|---|
| Restart Algorithm statistics | ||
| Number of algorithms provided | 2 | |
| Number of algorithms used | 1 | |
| Last algorithm used | /cpachecker/config/components/combinations-parallel-termination.properties | |
| Total time for algorithm 1 | 897.471s | |
| PredicateCPA statistics | ||
| Number of abstractions | 728 | 5% of all post computations |
| Times abstraction was reused | 0 | |
| Because of function entry/exit | 0 | 0% |
| Because of loop head | 397 | 55% |
| Because of join nodes | 0 | 0% |
| Because of threshold | 0 | 0% |
| Because of target state | 331 | 45% |
| Times precision was empty | 11 | 2% |
| Times precision was {false} | 328 | 45% |
| Times result was cached | 1 | 0% |
| Times cartesian abs was used | 0 | 0% |
| Times boolean abs was used | 388 | 53% |
| Times result was 'false' | 249 | 34% |
| Number of strengthen sat checks | 0 | |
| Number of coverage checks | 182099 | |
| BDD entailment checks | 11846 | |
| Number of SMT sat checks | 0 | |
| trivial | 0 | |
| cached | 0 | |
| Max ABE block size | 13 | |
| Avg ABE block size | 6.39 | sum: 4650, count: 728, min: 0, max: 13 |
| Number of predicates discovered | 93 | |
| Number of abstraction locations | 2 | |
| Max number of predicates per location | 93 | |
| Avg number of predicates per location | 47 | |
| Total predicates per abstraction | 26260 | |
| Max number of predicates per abstraction | 93 | |
| Avg number of predicates per abstraction | 36.68 | |
| Number of irrelevant predicates | 805 | 3% |
| Number of preds handled by boolean abs | 25451 | 97% |
| Total number of models for allsat | 27593 | |
| Max number of models for allsat | 1275 | |
| Avg number of models for allsat | 71.12 | |
| Time for post operator | 1.229s | |
| Time for path formula creation | 1.214s | |
| Time for strengthen operator | 0.258s | |
| Time for prec operator | 21.150s | |
| Time for abstraction | 21.019s | Max: 1.001s, Count: 728 |
| Boolean abstraction | 16.907s | |
| Solving time | 2.110s | Max: 0.013s |
| Model enumeration time | 15.098s | |
| Time for BDD construction | 4.118s | Max: 0.038s |
| Time for merge operator | 0.071s | |
| Time for coverage checks | 0.119s | |
| Time for BDD entailment checks | 0.101s | |
| Total time for SMT solver (w/o itp) | 17.208s | |
| Number of path formula cache hits | 9652 | 48% |
| Inside post operator | ||
| Inside path formula creation | ||
| Time for path formula computation | 1.179s | |
| Total number of created targets for pointer analysis | 0 | |
| Number of BDD nodes | 205476 | |
| Size of BDD node table | 466043 | |
| Size of BDD cache | 46619 | |
| Size of BDD node cleanup queue | 2.16 | sum: 262783, count: 121752, min: 0, max: 16573 |
| Time for BDD node cleanup | 0.036s | |
| Time for BDD garbage collection | 0.172s | in 52 runs |
| KeyValue statistics | ||
| Init. function predicates | 0 | |
| Init. global predicates | 0 | |
| Init. location predicates | 0 | |
| Invariant Generation statistics | ||
| AutomatonAnalysis (NonTerminationLabelAutomaton) statistics | ||
| Number of states | 1 | |
| Total time for successor computation | 0.172s | |
| Automaton transfers with branching | 0 | |
| Automaton transfer successors | 1.00 | sum: 13966, count: 13966, min: 1, max: 1 [1 x 13966] |
| Number of states with assumption transitions | 0 | |
| AutomatonAnalysis (TerminatingFunctions) statistics | ||
| Number of states | 1 | |
| Total time for successor computation | 0.019s | |
| Automaton transfers with branching | 0 | |
| Automaton transfer successors | 1.00 | sum: 13966, count: 13966, min: 1, max: 1 [1 x 13966] |
| Number of states with assumption transitions | 0 | |
| Termination Algorithm statistics | ||
| Total time | 136.637s | |
| Time for recursion analysis | 0.000s | |
| Number of analysed loops | 1 | 100% |
| Total time for loop analysis | 136.630s | |
| Avg time per loop analysis | 136.630s | |
| Max time per loop analysis | 136.630s | |
| Number of safety analysis runs | 70 | |
| Avg safety analysis run per loop | 70.00 | |
| Max safety analysis run per loop | 70 for loops [N7] | |
| Total time for safety analysis | 28.061s | |
| Avg time per safety analysis run | 0.400s | |
| Max time per safety analysis run | 1.464s | |
| Number of analysed lassos | 71 | |
| Avg number of lassos per loop | 71.00 | |
| Max number of lassos per loop | 71 for loops [N7] | |
| Avg number of lassos per iteration | 1.01 | |
| Max number of lassos per iteration | 2 | |
| Total time for lassos analysis | 108.385s | |
| Avg time per iteration | 1.548s | |
| Max time per iteration | 4.561s | |
| Time for lassos construction | 4.519s | |
| Avg time for lasso construction per iteration | 0.064s | |
| Max time for lasso construction per iteration | 0.358s | |
| Time for stem and loop construction | 0.279s | |
| Avg time for stem and loop construction per iteration | 0.003s | |
| Max time for stem and loop construction per iteration | 0.030s | |
| Time for lassos creation | 4.237s | |
| Avg time for lassos creation per iteration | 0.060s | |
| Max time for lassos creation per iteration | 0.357s | |
| Total time for non-termination analysis | 9.402s | |
| Avg time for non-termination analysis per lasso | 0.132s | |
| Max time for non-termination analysis per lasso | 0.173s | |
| Total time for termination analysis | 94.463s | |
| Avg time for termination analysis per lasso | 1.349s | |
| Max time for termination analysis per lasso | 4.330s | |
| Total number of termination arguments | 5 | |
| Avg termination arguments per loop | 5.00 | |
| Max termination arguments per loop | 5 for loops [N7] | |
| affine | 5 | |
| Counterexample-Check Algorithm statistics | ||
| Number of counterexample checks | 1 | |
| Number of infeasible paths | 0 | 0% |
| Time for counterexample checks | 759.813s | |
| Termination Algorithm statistics | ||
| Total time | 136.637s | |
| Time for recursion analysis | 0.000s | |
| Number of analysed loops | 1 | 100% |
| Total time for loop analysis | 136.630s | |
| Avg time per loop analysis | 136.630s | |
| Max time per loop analysis | 136.630s | |
| Number of safety analysis runs | 70 | |
| Avg safety analysis run per loop | 70.00 | |
| Max safety analysis run per loop | 70 for loops [N7] | |
| Total time for safety analysis | 28.061s | |
| Avg time per safety analysis run | 0.400s | |
| Max time per safety analysis run | 1.464s | |
| Number of analysed lassos | 71 | |
| Avg number of lassos per loop | 71.00 | |
| Max number of lassos per loop | 71 for loops [N7] | |
| Avg number of lassos per iteration | 1.01 | |
| Max number of lassos per iteration | 2 | |
| Total time for lassos analysis | 108.385s | |
| Avg time per iteration | 1.548s | |
| Max time per iteration | 4.561s | |
| Time for lassos construction | 4.519s | |
| Avg time for lasso construction per iteration | 0.064s | |
| Max time for lasso construction per iteration | 0.358s | |
| Time for stem and loop construction | 0.279s | |
| Avg time for stem and loop construction per iteration | 0.003s | |
| Max time for stem and loop construction per iteration | 0.030s | |
| Time for lassos creation | 4.237s | |
| Avg time for lassos creation per iteration | 0.060s | |
| Max time for lassos creation per iteration | 0.357s | |
| Total time for non-termination analysis | 9.402s | |
| Avg time for non-termination analysis per lasso | 0.132s | |
| Max time for non-termination analysis per lasso | 0.173s | |
| Total time for termination analysis | 94.463s | |
| Avg time for termination analysis per lasso | 1.349s | |
| Max time for termination analysis per lasso | 4.330s | |
| Total number of termination arguments | 5 | |
| Avg termination arguments per loop | 5.00 | |
| Max termination arguments per loop | 5 for loops [N7] | |
| affine | 5 | |
| Counterexample-Check Algorithm statistics | ||
| Number of counterexample checks | 1 | |
| Number of infeasible paths | 0 | 0% |
| Time for counterexample checks | 759.813s | |
| Code Coverage | ||
| Function coverage | 1.000 | |
| Visited lines | 14 | |
| Total lines | 14 | |
| Line coverage | 1.000 | |
| Visited conditions | 8 | |
| Total conditions | 8 | |
| Condition coverage | 1.000 | |
| CPAchecker general statistics | ||
| Number of program locations | 26 | |
| Number of CFA edges (per node) | 29 | count: 26, min: 0, max: 2, avg: 1.12 |
| Number of relevant variables | 2 | |
| Number of functions | 1 | |
| Number of loops (and loop nodes) | 1 | sum: 13, min: 13, max: 13, avg: 13.00 |
| Size of reached set | 1812 | |
| Number of reached locations | 18 | 69% |
| Avg states per location | 100 | |
| Max states per location | 146 | at node N8 |
| Number of reached functions | 1 | 100% |
| Number of partitions | 18 | |
| Avg size of partitions | 100 | |
| Max size of partitions | 146 | with key N8 |
| Number of target states | 1 | |
| Size of final wait list | 10 | |
| Time for analysis setup | 0.999s | |
| Time for loading CPAs | 0.016s | |
| Time for loading parser | 0.227s | |
| Time for CFA construction | 0.707s | |
| Time for parsing file(s) | 0.256s | |
| Time for AST to CFA | 0.172s | |
| Time for CFA sanity check | 0.019s | |
| Time for post-processing | 0.121s | |
| Time for loop structure | 0.005s | |
| Time for AST structure | 0.000s | |
| Time for CFA export | 0.429s | |
| Time for function pointers resolving | 0.003s | |
| Function calls via function pointers | 0 | count: 1, min: 0, max: 0, avg: 0.00 |
| Instrumented function pointer calls | 0 | count: 1, min: 0, max: 0, avg: 0.00 |
| Function calls with function pointer arguments | 0 | count: 1, min: 0, max: 0, avg: 0.00 |
| Instrumented function pointer arguments | 0 | count: 1, min: 0, max: 0, avg: 0.00 |
| Time for classifying variables | 0.076s | |
| Time for collecting variables | 0.049s | |
| Time for solving dependencies | 0.003s | |
| Time for building hierarchy | 0.000s | |
| Time for building classification | 0.020s | |
| Time for exporting data | 0.003s | |
| Time for Analysis | 897.472s | |
| CPU time for analysis | 850.940s | |
| Total time for CPAchecker | 898.481s | |
| Total CPU time for CPAchecker | 852.620s | |
| Time for statistics | 0.672s | |
| Time for Garbage Collector | 3.269s | in 1952 runs |
| Garbage Collector(s) used | PS MarkSweep, PS Scavenge | |
| Used heap memory | 372MB ( 355 MiB) max; 272MB ( 260 MiB) avg; 444MB ( 423 MiB) peak | |
| Used non-heap memory | 73MB ( 70 MiB) max; 70MB ( 66 MiB) avg; 74MB ( 70 MiB) peak | |
| Used in PS Old Gen pool | 341MB ( 325 MiB) max; 255MB ( 243 MiB) avg; 352MB ( 336 MiB) peak | |
| Allocated heap memory | 821MB ( 783 MiB) max; 692MB ( 660 MiB) avg | |
| Allocated non-heap memory | 75MB ( 71 MiB) max; 73MB ( 70 MiB) avg | |
| Total process virtual memory | 16365MB ( 15607 MiB) max; 16273MB ( 15519 MiB) avg |
| # | Configuration Name | Configuration Value |
|---|---|---|
| 1 | analysis.algorithm.termination | true |
| 2 | analysis.machineModel | Linux64 |
| 3 | analysis.name | terminationAnalysis |
| 4 | analysis.programNames | Benchmarks/TermCOMP/C/Stroeder_15/Ex08/Ex08.c |
| 5 | analysis.restartAfterUnknown | true |
| 6 | counterexample.export.exportWitness | false |
| 7 | cpa.arg.lateMerge | prevent |
| 8 | language | C |
| 9 | log.level | INFO |
| 10 | parser.usePreprocessor | true |
| 11 | restartAlgorithm.configFiles | components/combinations-parallel-termination.properties, components/termination-recursion.properties::if-recursive |
| 12 | specification | |
| 13 | statistics.print | true |
| 14 | termination.config | terminationAnalysis.properties |
This table was generated by CPAchecker. For feedback, questions, and bug reports please use our issue tracker.
License: Apache 2.0 License
Source: {{dependency.repository}}
{{dependency.copyright}}
License:
Full text of license
{{dependencies.licenses[dependency.licenseId]}}